\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$, $B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$),\+
\\[0ex]$f$:(($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$).
\-\\[0ex]ecl{-}trans{-}normal($A$)
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal($B$)
\\[0ex]$\Rightarrow$ ($\forall$$m$:$\mathbb{N}$. $\neg$$f$(($\lambda$$n$.false$_{2}$),$\lambda$$n$.false$_{2}$,$m$))
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal(combine{-}ecl{-}tuples($A$;$B$;$f$;$g$))
\end{tabbing}